The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

Rewrite Strategy: FULL

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
append(cons(y, ys), x) →⁺ cons(y, append(ys, x))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [ys / cons(y, ys)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

S is empty.
Rewrite Strategy: FULL

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

TRS:
Rules:
isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

Types:
isEmpty :: empty:node:y → true:false
empty :: empty:node:y
true :: true:false
node :: empty:node:y → elem → empty:node:y → empty:node:y
false :: true:false
left :: empty:node:y → empty:node:y
right :: empty:node:y → empty:node:y
elem :: empty:node:y → elem
append :: nil:cons → empty:node:y → nil:cons
nil :: nil:cons
cons :: empty:node:y → nil:cons → nil:cons
y :: empty:node:y
listify :: empty:node:y → nil:cons → nil:cons
if :: true:false → true:false → empty:node:y → empty:node:y → nil:cons → nil:cons → nil:cons
toList :: empty:node:y → nil:cons
hole_true:false1_0 :: true:false
hole_empty:node:y2_0 :: empty:node:y
hole_elem3_0 :: elem
hole_nil:cons4_0 :: nil:cons
gen_empty:node:y5_0 :: Nat → empty:node:y
gen_nil:cons6_0 :: Nat → nil:cons

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
append, listify

They will be analysed ascendingly in the following order:
append < listify

(8) Obligation:

TRS:
Rules:
isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

Types:
isEmpty :: empty:node:y → true:false
empty :: empty:node:y
true :: true:false
node :: empty:node:y → elem → empty:node:y → empty:node:y
false :: true:false
left :: empty:node:y → empty:node:y
right :: empty:node:y → empty:node:y
elem :: empty:node:y → elem
append :: nil:cons → empty:node:y → nil:cons
nil :: nil:cons
cons :: empty:node:y → nil:cons → nil:cons
y :: empty:node:y
listify :: empty:node:y → nil:cons → nil:cons
if :: true:false → true:false → empty:node:y → empty:node:y → nil:cons → nil:cons → nil:cons
toList :: empty:node:y → nil:cons
hole_true:false1_0 :: true:false
hole_empty:node:y2_0 :: empty:node:y
hole_elem3_0 :: elem
hole_nil:cons4_0 :: nil:cons
gen_empty:node:y5_0 :: Nat → empty:node:y
gen_nil:cons6_0 :: Nat → nil:cons

Generator Equations:
gen_empty:node:y5_0(0) ⇔ empty
gen_empty:node:y5_0(+(x, 1)) ⇔ node(empty, hole_elem3_0, gen_empty:node:y5_0(x))
gen_nil:cons6_0(0) ⇔ nil
gen_nil:cons6_0(+(x, 1)) ⇔ cons(empty, gen_nil:cons6_0(x))

The following defined symbols remain to be analysed:
append, listify

They will be analysed ascendingly in the following order:
append < listify

(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol append.

(10) Obligation:

TRS:
Rules:
isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

Types:
isEmpty :: empty:node:y → true:false
empty :: empty:node:y
true :: true:false
node :: empty:node:y → elem → empty:node:y → empty:node:y
false :: true:false
left :: empty:node:y → empty:node:y
right :: empty:node:y → empty:node:y
elem :: empty:node:y → elem
append :: nil:cons → empty:node:y → nil:cons
nil :: nil:cons
cons :: empty:node:y → nil:cons → nil:cons
y :: empty:node:y
listify :: empty:node:y → nil:cons → nil:cons
if :: true:false → true:false → empty:node:y → empty:node:y → nil:cons → nil:cons → nil:cons
toList :: empty:node:y → nil:cons
hole_true:false1_0 :: true:false
hole_empty:node:y2_0 :: empty:node:y
hole_elem3_0 :: elem
hole_nil:cons4_0 :: nil:cons
gen_empty:node:y5_0 :: Nat → empty:node:y
gen_nil:cons6_0 :: Nat → nil:cons

Generator Equations:
gen_empty:node:y5_0(0) ⇔ empty
gen_empty:node:y5_0(+(x, 1)) ⇔ node(empty, hole_elem3_0, gen_empty:node:y5_0(x))
gen_nil:cons6_0(0) ⇔ nil
gen_nil:cons6_0(+(x, 1)) ⇔ cons(empty, gen_nil:cons6_0(x))

The following defined symbols remain to be analysed:
listify

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol listify.

(12) Obligation:

TRS:
Rules:
isEmpty(empty) → true
isEmpty(node(l, x, r)) → false
left(empty) → empty
left(node(l, x, r)) → l
right(empty) → empty
right(node(l, x, r)) → r
elem(node(l, x, r)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
listify(n, xs) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))), xs, append(xs, n))
if(true, b, n, m, xs, ys) → xs
if(false, false, n, m, xs, ys) → listify(m, xs)
if(false, true, n, m, xs, ys) → listify(n, ys)
toList(n) → listify(n, nil)

Types:
isEmpty :: empty:node:y → true:false
empty :: empty:node:y
true :: true:false
node :: empty:node:y → elem → empty:node:y → empty:node:y
false :: true:false
left :: empty:node:y → empty:node:y
right :: empty:node:y → empty:node:y
elem :: empty:node:y → elem
append :: nil:cons → empty:node:y → nil:cons
nil :: nil:cons
cons :: empty:node:y → nil:cons → nil:cons
y :: empty:node:y
listify :: empty:node:y → nil:cons → nil:cons
if :: true:false → true:false → empty:node:y → empty:node:y → nil:cons → nil:cons → nil:cons
toList :: empty:node:y → nil:cons
hole_true:false1_0 :: true:false
hole_empty:node:y2_0 :: empty:node:y
hole_elem3_0 :: elem
hole_nil:cons4_0 :: nil:cons
gen_empty:node:y5_0 :: Nat → empty:node:y
gen_nil:cons6_0 :: Nat → nil:cons

Generator Equations:
gen_empty:node:y5_0(0) ⇔ empty
gen_empty:node:y5_0(+(x, 1)) ⇔ node(empty, hole_elem3_0, gen_empty:node:y5_0(x))
gen_nil:cons6_0(0) ⇔ nil
gen_nil:cons6_0(+(x, 1)) ⇔ cons(empty, gen_nil:cons6_0(x))

No more defined symbols left to analyse.